H-Termination proof of /home/matraf/haskell/eval_FullyBlown

MAYBE 2.142 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ BR

mainModule Main

((enumFromThenTo :: () -> () -> () -> [()]) :: () -> () -> () -> [()])

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((enumFromThenTo :: () -> () -> () -> [()]) :: () -> () -> () -> [()])

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

p

| n' >= n

= flip (<=) m

| otherwise

= flip (>=) m

is transformed to

p = p2

p0 True = flip (>=) m

p1 True = flip (<=) m

p1 False = p0 otherwise

p2 = p1 (n' >= n)

The following Function with conditions

takeWhile p [] = []

takeWhile p (x : xs)

| p x

= x : takeWhile p xs

| otherwise

= []

is transformed to

takeWhile p [] = takeWhile3 p []

takeWhile p (x : xs) = takeWhile2 p (x : xs)

takeWhile0 p x xs True = []

takeWhile1 p x xs True = x : takeWhile p xs

takeWhile1 p x xs False = takeWhile0 p x xs otherwise

takeWhile2 p (x : xs) = takeWhile1 p x xs (p x)

takeWhile3 p [] = []

takeWhile3 wv ww = takeWhile2 wv ww

The following Function with conditions

toEnum 0 = ()

is transformed to

toEnum wx = toEnum1 wx

toEnum0 True wx = ()

toEnum1 wx = toEnum0 (wx == 0) wx

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

mainModule Main

((enumFromThenTo :: () -> () -> () -> [()]) :: () -> () -> () -> [()])

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

takeWhile p (numericEnumFromThen n n')

where

p = p2

p0 True = flip (>=) m

p1 True = flip (<=) m

p1 False = p0 otherwise

p2 = p1 (n' >= n)

are unpacked to the following functions on top level

numericEnumFromThenToP1 wy wz xu True = flip (<=) wy

numericEnumFromThenToP1 wy wz xu False = numericEnumFromThenToP0 wy wz xu otherwise

numericEnumFromThenToP2 wy wz xu = numericEnumFromThenToP1 wy wz xu (wz >= xu)

numericEnumFromThenToP wy wz xu = numericEnumFromThenToP2 wy wz xu

numericEnumFromThenToP0 wy wz xu True = flip (>=) wy

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

mainModule Main

((enumFromThenTo :: () -> () -> () -> [()]) :: () -> () -> () -> [()])

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                  ↳ Narrow

mainModule Main

(enumFromThenTo :: () -> () -> () -> [()])

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="enumFromThenTo",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="enumFromThenTo xv3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="enumFromThenTo xv3 xv4",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="enumFromThenTo xv3 xv4 xv5",fontsize=16,color="black",shape="triangle"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="map toEnum (enumFromThenTo (fromEnum xv3) (fromEnum xv4) (fromEnum xv5))",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="map toEnum (numericEnumFromThenTo (fromEnum xv3) (fromEnum xv4) (fromEnum xv5))",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="map toEnum (takeWhile (numericEnumFromThenToP (fromEnum xv5) (fromEnum xv4) (fromEnum xv3)) (numericEnumFromThen (fromEnum xv3) (fromEnum xv4)))",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="map toEnum (takeWhile (numericEnumFromThenToP (fromEnum xv5) (fromEnum xv4) (fromEnum xv3)) (iterate (fromEnum xv4 - fromEnum xv3 +) (fromEnum xv3)))",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="map toEnum (takeWhile (numericEnumFromThenToP (fromEnum xv5) (fromEnum xv4) (fromEnum xv3)) (fromEnum xv3 : iterate (fromEnum xv4 - fromEnum xv3 +) (fromEnum xv4 - fromEnum xv3 + fromEnum xv3)))",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="map toEnum (takeWhile2 (numericEnumFromThenToP (fromEnum xv5) (fromEnum xv4) (fromEnum xv3)) (fromEnum xv3 : iterate (fromEnum xv4 - fromEnum xv3 +) (fromEnum xv4 - fromEnum xv3 + fromEnum xv3)))",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="map toEnum (takeWhile1 (numericEnumFromThenToP (fromEnum xv5) (fromEnum xv4) (fromEnum xv3)) (fromEnum xv3) (iterate (fromEnum xv4 - fromEnum xv3 +) (fromEnum xv4 - fromEnum xv3 + fromEnum xv3)) (numericEnumFromThenToP (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (fromEnum xv3)))",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="map toEnum (takeWhile1 (numericEnumFromThenToP2 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3)) (fromEnum xv3) (iterate (fromEnum xv4 - fromEnum xv3 +) (fromEnum xv4 - fromEnum xv3 + fromEnum xv3)) (numericEnumFromThenToP2 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (fromEnum xv3)))",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (fromEnum xv4 >= fromEnum xv3)) (fromEnum xv3) (iterate (fromEnum xv4 - fromEnum xv3 +) (fromEnum xv4 - fromEnum xv3 + fromEnum xv3)) (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (fromEnum xv4 >= fromEnum xv3) (fromEnum xv3)))",fontsize=16,color="black",shape="box"];14 -> 15[label="",style="solid", color="black", weight=3];
15[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (compare (fromEnum xv4) (fromEnum xv3) /= LT)) (fromEnum xv3) (iterate (fromEnum xv4 - fromEnum xv3 +) (fromEnum xv4 - fromEnum xv3 + fromEnum xv3)) (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (compare (fromEnum xv4) (fromEnum xv3) /= LT) (fromEnum xv3)))",fontsize=16,color="black",shape="box"];15 -> 16[label="",style="solid", color="black", weight=3];
16[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (not (compare (fromEnum xv4) (fromEnum xv3) == LT))) (fromEnum xv3) (iterate (fromEnum xv4 - fromEnum xv3 +) (fromEnum xv4 - fromEnum xv3 + fromEnum xv3)) (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (not (compare (fromEnum xv4) (fromEnum xv3) == LT)) (fromEnum xv3)))",fontsize=16,color="black",shape="box"];16 -> 17[label="",style="solid", color="black", weight=3];
17[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (not (primCmpInt (fromEnum xv4) (fromEnum xv3) == LT))) (fromEnum xv3) (iterate (fromEnum xv4 - fromEnum xv3 +) (fromEnum xv4 - fromEnum xv3 + fromEnum xv3)) (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum xv4) (fromEnum xv3) (not (primCmpInt (fromEnum xv4) (fromEnum xv3) == LT)) (fromEnum xv3)))",fontsize=16,color="burlywood",shape="box"];71[label="xv4/()",fontsize=10,color="white",style="solid",shape="box"];17 -> 71[label="",style="solid", color="burlywood", weight=9];
71 -> 18[label="",style="solid", color="burlywood", weight=3];
18[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum ()) (fromEnum xv3) (not (primCmpInt (fromEnum ()) (fromEnum xv3) == LT))) (fromEnum xv3) (iterate (fromEnum () - fromEnum xv3 +) (fromEnum () - fromEnum xv3 + fromEnum xv3)) (numericEnumFromThenToP1 (fromEnum xv5) (fromEnum ()) (fromEnum xv3) (not (primCmpInt (fromEnum ()) (fromEnum xv3) == LT)) (fromEnum xv3)))",fontsize=16,color="black",shape="box"];18 -> 19[label="",style="solid", color="black", weight=3];
19[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (fromEnum xv3) (not (primCmpInt (Pos Zero) (fromEnum xv3) == LT))) (fromEnum xv3) (iterate (Pos Zero - fromEnum xv3 +) (Pos Zero - fromEnum xv3 + fromEnum xv3)) (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (fromEnum xv3) (not (primCmpInt (Pos Zero) (fromEnum xv3) == LT)) (fromEnum xv3)))",fontsize=16,color="burlywood",shape="box"];72[label="xv3/()",fontsize=10,color="white",style="solid",shape="box"];19 -> 72[label="",style="solid", color="burlywood", weight=9];
72 -> 20[label="",style="solid", color="burlywood", weight=3];
20[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (fromEnum ()) (not (primCmpInt (Pos Zero) (fromEnum ()) == LT))) (fromEnum ()) (iterate (Pos Zero - fromEnum () +) (Pos Zero - fromEnum () + fromEnum ())) (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (fromEnum ()) (not (primCmpInt (Pos Zero) (fromEnum ()) == LT)) (fromEnum ())))",fontsize=16,color="black",shape="box"];20 -> 21[label="",style="solid", color="black", weight=3];
21[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos Zero) == LT))) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (Pos Zero) (not (primCmpInt (Pos Zero) (Pos Zero) == LT)) (Pos Zero)))",fontsize=16,color="black",shape="box"];21 -> 22[label="",style="solid", color="black", weight=3];
22[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (Pos Zero) (not (EQ == LT))) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (Pos Zero) (not (EQ == LT)) (Pos Zero)))",fontsize=16,color="black",shape="box"];22 -> 23[label="",style="solid", color="black", weight=3];
23[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (Pos Zero) (not False)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (Pos Zero) (not False) (Pos Zero)))",fontsize=16,color="black",shape="box"];23 -> 24[label="",style="solid", color="black", weight=3];
24[label="map toEnum (takeWhile1 (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (Pos Zero) True) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (numericEnumFromThenToP1 (fromEnum xv5) (Pos Zero) (Pos Zero) True (Pos Zero)))",fontsize=16,color="black",shape="box"];24 -> 25[label="",style="solid", color="black", weight=3];
25[label="map toEnum (takeWhile1 (flip (<=) (fromEnum xv5)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (flip (<=) (fromEnum xv5) (Pos Zero)))",fontsize=16,color="black",shape="box"];25 -> 26[label="",style="solid", color="black", weight=3];
26[label="map toEnum (takeWhile1 (flip (<=) (fromEnum xv5)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) ((<=) Pos Zero fromEnum xv5))",fontsize=16,color="black",shape="box"];26 -> 27[label="",style="solid", color="black", weight=3];
27[label="map toEnum (takeWhile1 (flip (<=) (fromEnum xv5)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (compare (Pos Zero) (fromEnum xv5) /= GT))",fontsize=16,color="black",shape="box"];27 -> 28[label="",style="solid", color="black", weight=3];
28[label="map toEnum (takeWhile1 (flip (<=) (fromEnum xv5)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (not (compare (Pos Zero) (fromEnum xv5) == GT)))",fontsize=16,color="black",shape="box"];28 -> 29[label="",style="solid", color="black", weight=3];
29[label="map toEnum (takeWhile1 (flip (<=) (fromEnum xv5)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (not (primCmpInt (Pos Zero) (fromEnum xv5) == GT)))",fontsize=16,color="burlywood",shape="box"];73[label="xv5/()",fontsize=10,color="white",style="solid",shape="box"];29 -> 73[label="",style="solid", color="burlywood", weight=9];
73 -> 30[label="",style="solid", color="burlywood", weight=3];
30[label="map toEnum (takeWhile1 (flip (<=) (fromEnum ())) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (not (primCmpInt (Pos Zero) (fromEnum ()) == GT)))",fontsize=16,color="black",shape="box"];30 -> 31[label="",style="solid", color="black", weight=3];
31[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (not (primCmpInt (Pos Zero) (Pos Zero) == GT)))",fontsize=16,color="black",shape="box"];31 -> 32[label="",style="solid", color="black", weight=3];
32[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (not (EQ == GT)))",fontsize=16,color="black",shape="box"];32 -> 33[label="",style="solid", color="black", weight=3];
33[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) (not False))",fontsize=16,color="black",shape="box"];33 -> 34[label="",style="solid", color="black", weight=3];
34[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)) True)",fontsize=16,color="black",shape="box"];34 -> 35[label="",style="solid", color="black", weight=3];
35[label="map toEnum (Pos Zero : takeWhile (flip (<=) (Pos Zero)) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)))",fontsize=16,color="black",shape="box"];35 -> 36[label="",style="solid", color="black", weight=3];
36[label="toEnum (Pos Zero) : map toEnum (takeWhile (flip (<=) (Pos Zero)) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)))",fontsize=16,color="green",shape="box"];36 -> 37[label="",style="dashed", color="green", weight=3];
36 -> 38[label="",style="dashed", color="green", weight=3];
37[label="toEnum (Pos Zero)",fontsize=16,color="black",shape="triangle"];37 -> 39[label="",style="solid", color="black", weight=3];
38[label="map toEnum (takeWhile (flip (<=) (Pos Zero)) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + Pos Zero)))",fontsize=16,color="black",shape="box"];38 -> 40[label="",style="solid", color="black", weight=3];
39[label="toEnum1 (Pos Zero)",fontsize=16,color="black",shape="box"];39 -> 41[label="",style="solid", color="black", weight=3];
40[label="map toEnum (takeWhile (flip (<=) (Pos Zero)) (Pos Zero - Pos Zero + Pos Zero : iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + (Pos Zero - Pos Zero + Pos Zero))))",fontsize=16,color="black",shape="box"];40 -> 42[label="",style="solid", color="black", weight=3];
41[label="toEnum0 (Pos Zero == Pos Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];41 -> 43[label="",style="solid", color="black", weight=3];
42[label="map toEnum (takeWhile2 (flip (<=) (Pos Zero)) (Pos Zero - Pos Zero + Pos Zero : iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + (Pos Zero - Pos Zero + Pos Zero))))",fontsize=16,color="black",shape="box"];42 -> 44[label="",style="solid", color="black", weight=3];
43[label="toEnum0 (primEqInt (Pos Zero) (Pos Zero)) (Pos Zero)",fontsize=16,color="black",shape="box"];43 -> 45[label="",style="solid", color="black", weight=3];
44[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero - Pos Zero + Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + (Pos Zero - Pos Zero + Pos Zero))) (flip (<=) (Pos Zero) (Pos Zero - Pos Zero + Pos Zero)))",fontsize=16,color="black",shape="box"];44 -> 46[label="",style="solid", color="black", weight=3];
45[label="toEnum0 True (Pos Zero)",fontsize=16,color="black",shape="box"];45 -> 47[label="",style="solid", color="black", weight=3];
46[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero - Pos Zero + Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + (Pos Zero - Pos Zero + Pos Zero))) ((<=) Pos Zero - Pos Zero + Pos Zero Pos Zero))",fontsize=16,color="black",shape="box"];46 -> 48[label="",style="solid", color="black", weight=3];
47[label="()",fontsize=16,color="green",shape="box"];48[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero - Pos Zero + Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + (Pos Zero - Pos Zero + Pos Zero))) (compare (Pos Zero - Pos Zero + Pos Zero) (Pos Zero) /= GT))",fontsize=16,color="black",shape="box"];48 -> 49[label="",style="solid", color="black", weight=3];
49[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero - Pos Zero + Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + (Pos Zero - Pos Zero + Pos Zero))) (not (compare (Pos Zero - Pos Zero + Pos Zero) (Pos Zero) == GT)))",fontsize=16,color="black",shape="box"];49 -> 50[label="",style="solid", color="black", weight=3];
50[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero - Pos Zero + Pos Zero) (iterate (Pos Zero - Pos Zero +) (Pos Zero - Pos Zero + (Pos Zero - Pos Zero + Pos Zero))) (not (primCmpInt (Pos Zero - Pos Zero + Pos Zero) (Pos Zero) == GT)))",fontsize=16,color="black",shape="box"];50 -> 51[label="",style="solid", color="black", weight=3];
51[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (primPlusInt (Pos Zero - Pos Zero) (Pos Zero)) (iterate (primPlusInt (Pos Zero - Pos Zero)) (primPlusInt (Pos Zero - Pos Zero) (primPlusInt (Pos Zero - Pos Zero) (Pos Zero)))) (not (primCmpInt (primPlusInt (Pos Zero - Pos Zero) (Pos Zero)) (Pos Zero) == GT)))",fontsize=16,color="black",shape="box"];51 -> 52[label="",style="solid", color="black", weight=3];
52[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (primPlusInt (primMinusInt (Pos Zero) (Pos Zero)) (Pos Zero)) (iterate (primPlusInt (primMinusInt (Pos Zero) (Pos Zero))) (primPlusInt (primMinusInt (Pos Zero) (Pos Zero)) (primPlusInt (primMinusInt (Pos Zero) (Pos Zero)) (Pos Zero)))) (not (primCmpInt (primPlusInt (primMinusInt (Pos Zero) (Pos Zero)) (Pos Zero)) (Pos Zero) == GT)))",fontsize=16,color="black",shape="box"];52 -> 53[label="",style="solid", color="black", weight=3];
53[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (primPlusInt (primMinusNat Zero Zero) (Pos Zero)) (iterate (primPlusInt (primMinusNat Zero Zero)) (primPlusInt (primMinusNat Zero Zero) (primPlusInt (primMinusNat Zero Zero) (Pos Zero)))) (not (primCmpInt (primPlusInt (primMinusNat Zero Zero) (Pos Zero)) (Pos Zero) == GT)))",fontsize=16,color="black",shape="box"];53 -> 54[label="",style="solid", color="black", weight=3];
54[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (primPlusInt (Pos Zero) (Pos Zero)))) (not (primCmpInt (primPlusInt (Pos Zero) (Pos Zero)) (Pos Zero) == GT)))",fontsize=16,color="black",shape="triangle"];54 -> 55[label="",style="solid", color="black", weight=3];
55[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos (primPlusNat Zero Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (Pos (primPlusNat Zero Zero)))) (not (primCmpInt (Pos (primPlusNat Zero Zero)) (Pos Zero) == GT)))",fontsize=16,color="black",shape="box"];55 -> 56[label="",style="solid", color="black", weight=3];
56[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero))) (not (primCmpInt (Pos Zero) (Pos Zero) == GT)))",fontsize=16,color="black",shape="box"];56 -> 57[label="",style="solid", color="black", weight=3];
57[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero))) (not (EQ == GT)))",fontsize=16,color="black",shape="box"];57 -> 58[label="",style="solid", color="black", weight=3];
58[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero))) (not False))",fontsize=16,color="black",shape="box"];58 -> 59[label="",style="solid", color="black", weight=3];
59[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero))) True)",fontsize=16,color="black",shape="box"];59 -> 60[label="",style="solid", color="black", weight=3];
60[label="map toEnum (Pos Zero : takeWhile (flip (<=) (Pos Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero))))",fontsize=16,color="black",shape="box"];60 -> 61[label="",style="solid", color="black", weight=3];
61[label="toEnum (Pos Zero) : map toEnum (takeWhile (flip (<=) (Pos Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero))))",fontsize=16,color="green",shape="box"];61 -> 62[label="",style="dashed", color="green", weight=3];
61 -> 63[label="",style="dashed", color="green", weight=3];
62 -> 37[label="",style="dashed", color="red", weight=0];
62[label="toEnum (Pos Zero)",fontsize=16,color="magenta"];63[label="map toEnum (takeWhile (flip (<=) (Pos Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero))))",fontsize=16,color="black",shape="box"];63 -> 64[label="",style="solid", color="black", weight=3];
64[label="map toEnum (takeWhile (flip (<=) (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero) : iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (primPlusInt (Pos Zero) (Pos Zero)))))",fontsize=16,color="black",shape="box"];64 -> 65[label="",style="solid", color="black", weight=3];
65[label="map toEnum (takeWhile2 (flip (<=) (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero) : iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (primPlusInt (Pos Zero) (Pos Zero)))))",fontsize=16,color="black",shape="box"];65 -> 66[label="",style="solid", color="black", weight=3];
66[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (primPlusInt (Pos Zero) (Pos Zero)))) (flip (<=) (Pos Zero) (primPlusInt (Pos Zero) (Pos Zero))))",fontsize=16,color="black",shape="box"];66 -> 67[label="",style="solid", color="black", weight=3];
67[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (primPlusInt (Pos Zero) (Pos Zero)))) ((<=) primPlusInt (Pos Zero) (Pos Zero) Pos Zero))",fontsize=16,color="black",shape="box"];67 -> 68[label="",style="solid", color="black", weight=3];
68[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (primPlusInt (Pos Zero) (Pos Zero)))) (compare (primPlusInt (Pos Zero) (Pos Zero)) (Pos Zero) /= GT))",fontsize=16,color="black",shape="box"];68 -> 69[label="",style="solid", color="black", weight=3];
69[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (primPlusInt (Pos Zero) (Pos Zero)))) (not (compare (primPlusInt (Pos Zero) (Pos Zero)) (Pos Zero) == GT)))",fontsize=16,color="black",shape="box"];69 -> 70[label="",style="solid", color="black", weight=3];
70 -> 54[label="",style="dashed", color="red", weight=0];
70[label="map toEnum (takeWhile1 (flip (<=) (Pos Zero)) (primPlusInt (Pos Zero) (Pos Zero)) (iterate (primPlusInt (Pos Zero)) (primPlusInt (Pos Zero) (primPlusInt (Pos Zero) (Pos Zero)))) (not (primCmpInt (primPlusInt (Pos Zero) (Pos Zero)) (Pos Zero) == GT)))",fontsize=16,color="magenta"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ QDP

                      ↳ NonTerminationProof

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_map → new_map

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_map → new_map

The TRS R consists of the following rules:none

s = new_map evaluates to t =new_map

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_map to new_map.

Haskell To QDPs

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ PisEmptyProof

                      ↳ QDP

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ LetRed

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

new_map([]) → new_map([])

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_map([]) → new_map([])

The TRS R consists of the following rules:none

s = new_map([]) evaluates to t =new_map([])

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_map([]) to new_map([]).

takeWhile	p []	= takeWhile3 p []
takeWhile	p (x : xs)	= takeWhile2 p (x : xs)

takeWhile1	p x xs True	= x : takeWhile p xs
takeWhile1	p x xs False	= takeWhile0 p x xs otherwise

numericEnumFromThenToP1	wy wz xu True	= flip (<=) wy
numericEnumFromThenToP1	wy wz xu False	= numericEnumFromThenToP0 wy wz xu otherwise